#include <iostream>
#include <stack>
#include <cuda_runtime_api.h>

#include "ProblemData.h"
#include "Node.h"

using namespace std;

int main (int argc, char * * argv)
{
	if (argc < 2 || argc > 4)
	{
		cerr << "Use : " << argv[0] << " <data_file> [<N>] [<parallel>]" << endl;
		exit(EXIT_FAILURE);
	}
	
	unsigned int N = 1;
	bool parallel = false;
	if (argc >= 3)
	{
		long tmp = strtol(argv[2], NULL, 10);
		if (tmp <= 0)
		{
			cerr << "Error: N should be a positive integer" << endl;
			exit(EXIT_FAILURE);
		}
		N = (int) tmp;

		if (argc == 4)
		{
			if (strtol(argv[3], NULL, 10) != 0)
			{
				parallel = true;
			}
		}
	}
	
	/* Open the data file. */
	ProblemData data(argv[1]);
	data.print();

	stack<Node> nodes;
	bool is_solved = false;
	Node *solution = NULL;
	nodes.push(Node::getFirstNode(data));
	
	/* While no valid affectation has been found and there still are some nodes
	   to explore
	 */
	
	if(nodes.top().isSolvable())
	{
		while (!is_solved && !nodes.empty())
		{
			/* Get the current node and pop it from the stack. */
			Node current_node = nodes.top();
			nodes.pop();
			
			/* Get the next variable that has to be affected and do the exploration
			 starting from the current node.
			 */
			vector<Node> affectations;
			if (!parallel)
			{
				affectations = current_node.explore(N);
			}
			else
			{
				affectations = current_node.exploreParallel(N);
			}
			
			/* Get the affectations that have been made and add the resulting nodes
			 to the stack (unless the formula has been satisfied).
			 */
			for (int i = (int) affectations.size() - 1; !is_solved && i >= 0; i--)
			{
				if (affectations[i].isSolved())
				{
					is_solved = true;
					solution = new Node(affectations[i]);
				}
				else if (affectations[i].unaffected(N) != 0)
				{
					nodes.push(affectations[i]);
				}
			}
		}
	}

	cudaDeviceReset();
	
	/* Print the solution if one was found or print that the formula is
	   unsatisfiable if none was found.
	 */
	if (is_solved)
	{
		cout << endl << "Formula is satisfiable." << endl << endl;
		cout << "Solution: ";
		solution->printSolution();
		data.checkSolution(*solution);
		solution->writeSolution("result.cnf");
		delete solution;
	}
	else
	{
		cout << endl << "Formula is unsatisfiable." << endl;
	}

	return 0;
}
